COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(
C00022 ENDMK
C⊗;
(
HELP
"This program is designed to be used as a tool for verification
of properties of PASCAL programs presented to it, along with
lemmas about those programs.  The most commonly used upper level
command is READ.  Type 'HELP WHAT;' for a list of help commands.
For help on topic X, assuming help data exists, type 'HELP X;'."

WHAT
"HELP messages are available for the following:
ALIAS   BUG     COMMANDS
DELRFILE	DELRULE		DOCUMENTATION
DUMP	DUMPVC	DUMPRULE	DUMPINTERNAL	DUMPSYMBOLS
LISP
LOAD	LOADVC	LOADRULE	LOADSYMBOLS
MANUAL	NEWS
PARSE   PREVIOUS	PRINTVC
READ	READVC
SHOW    SIMPINIT    SIMPLIFY    STATUS    SWITCHES	SYSTEM
TOPLEVEL	    VC
This file (which contains all the help routines) is NEWVER.HPT[1,3]."

ALIAS
"This command is used to change the default disk area used by DUMPVC,
DUMPRULE, LOADVC, and LOADRULE.  'ALIAS EX,VER;', for example, will
set [EX,VER] as the default area for these commands.  Of course, you
can override the default by specifying the area explicitly in one
of these commands.  'ALIAS;' will display your current default area.
The PARSE and READVC commands may or may not be affected by ALIAS.
This should change shortly."

BUG
"The BUG feature is provided to help verifier hackers make changes
to syntax, semantics, etc.  There are two user commands,
(SETBUG <number>) and (RESETBUG <number>), which set and then reset
the bug with the appropriate number.  See MEMO[VCG,RAK] to see which
bugs currently exist and what they do."

COMMANDS
"The following commands are available:
READ, READVC, LOAD(VC/RULE/TABLE), DUMP, SIMPLIFY, ALIAS, SHOW, STATUS,
DELRFILE, DELRULE, LISP.
For more information type HELP followed by the command, or read the
file TOPLEV[DOC,VER]."

DOCUMENTATION
"Files intended to be documentation on the verifier or portions 
thereof are kept in the directory [DOC,VER].  You might try looking
there for things.  Don't be too surprised if some large gaps exist.
The system toplevel is documented in TOPLEV[DOC,VER].
Here are a few other random places:
MEMO[VCG,RAK] -- about the parser, Pascal, etc.
SSEM[VCG,RAK] -- page 2 explains the structure of the symbol table
VERIFY.DOC[DOC,VER] -- Details about LOADVC, LOADRULE, DUMPVC, DUMPRULE,
	ALIAS.   Also information about examples in [EX,VER], hackery
	information, etc. "

DUMP
"The command DUMP is a combination of DUMPVC and DUMPRULE.
'DUMP FOO;' is equivalent to 'DUMPVC FOO;' followed by 'DUMPRULE FOO;'."

DUMPINTERNAL
"This command is either (DUMPINTERNAL T) or (DUMPINTERNAL NIL) to
turn the facility on or off; default is NIL.  DUMPINTERNAL causes
internal format output by the parser to be placed in the symbol
table for each procedure or function parsed.  It is generally only
useful in conjunction with dumping the symbol table (see DUMPSYMBOLS)
and the VC command (see VC). THIS COMMAND IS AVAILABLE AS A LISP
FUNCTION ONLY."

DUMPRULE
"The command DUMPRULE is used to dump a 'compiled' rulefile to disk.
It allows use of the standalone simplifier, VPROVE, and also saves
parse time because rulefiles need only be parsed once, then dumped.
The default filename is VERIFY.CRL in you aliased area.  The ALIAS
command affects DUMPRULE and LOADRULE.   This command should 
be used in conjunction with LOADRULE, which loads these 'compiled'
rulefiles.   Thus, you can parse a rulefile using VCGEN or VERIFY, 
do a DUMPRULE, and then load it via LOADRULE into either VPROVE 
or VERIFY.    Examples:  'DUMPRULE SORT;' makes SORT.CRL.
'DUMPRULE FOO.CRL[VER,BAR];' makes FOO.CRL[VER,BAR].   If more than
one rulefile exists, it will dump the most recent one parsed.  You may
also specify a rulefile name to DUMPRULE, as in 'DUMPRULE SORT, SORTRULES;'.
LOADRULE is used to load in these files (the same naming defaults apply)."

DUMPSYMBOLS
"The command DUMPSYMBOLS is optionally followed by a file in the
same format as PARSE.  It instructs the parser to dump code to that
file that will permit reloading the symbol table environment of all
the procedures in the file.  (DUMPSYMBOLS) turns off dumping.  So
does any subsequent attempt to load a symbol table file.  See
LOADSYMBOLS for information on how to load a symbol table."

DUMPVC
"The command DUMPVC is used to dump verification conditions into
a file.   It is usefule because it allows use of the standalone prover,
VPROVE, and because it saves parsing time by storing the VCs in their
internal format. The default extension is .CVC; thus 'DUMPVC FOO;'
writes on a file FOO.CVC.  If no filename is given, VERIFY.CVC in your
aliased area is used.  DUMPVC is affected by the ALIAS command, as is
LOADVC, its counterpart.  LOADVC is used to load these files.   Thus,
a program may be parsed with VCGEN or VERIFY, and the VCs dumped with 
DUMPVC.  The LOADVC may be used to load the VCs into VPROVE or VERIFY
for later use.   Examples:  'DUMPVC FOO;' puts the compiled VCs
into FOO.CVC in your aliased area.   'DUMPVC FOO.CVC[VER,BAR];'
puts them in FOO.CVC[VER,BAR].  LOADVC has a corresponding syntax."

LISP
"Although this is primarily a program verifier, it exists in a
MACLSP environment.  This means that the general facilities of
such LISP are available.  The command 'LISP;' returns control to the
MACLISP toplevel.  The file VERIFY.DOC[DOC,VER] contains
some advice about recovery from errors, etc. in MACLISP."

LOADRULE
"The command LOADRULE is used to load in files created with DUMPRULE.
See DUMPRULE for further information."

LOADSYMBOLS
"The command LOADSYMBOLS must be followed by two items: first a
procedure name and then a file.  The system will turn off symbol
table dumping (if it is on), clear the symbol table, and then attempt
to load the symbol table environment of the procedure specified from
the file given.  The format of the file name is the same as that of
the PARSE command. See DUMPSYMBOLS for information on how to create
a file that contains symbol table information."

LOADVC
"The command LOADVC is used to load in files created by DUMPVC.
See DUMPVC for further information."

MANUAL
"Unfortunately, manual mode is not up yet.  If you want to
implement it, talk to WLS."

NEWS
"The STATUS command displays info about VCs and rules loaded.
SHOW displays the values of system switches.
DELRULE rule deletes rule 'rule', and 'DELRFILE rfile;' deletes
the rulefile 'rfile'. For more info type 'HELP STATUS;' etc."
 
PARSE
"You should use READ instead of the internal PARSE command !!
The command (PARSE) accepts input from the teletype. (PARSE X)
will try to take input from the file X.  Here are some examples
for taking files with two word names and from another directory
(here p,pn is programmer,project and X Y is the two word file name
X.Y): (PARSE X Y), (PARSE X (P,PN)), and (PARSE X Y (P,PN))  .  
The parser calls the verification condition generator, but does
not do simplification.  For this, the command SIMPLIFY must be
used. The syntactic scan and semantic routines should NEVER
bomb out, no matter what string you give them.  If they do,
send a note to RAK and SAVE the program!!!"

PREVIOUS
"The command (PREVIOUS <positive integer>) has meaning when a
syntax scan finds a syntax error.  It will print out as many
tokens preceding the syntax error as it is asked (if there are
that many).  (PREVIOUS 10) is called in the errorhandling.  As
the number of tokens requested increases, time to find them can
go up alarmingly. After an error and before parsing something
else, previous may be called as many times as desired."

PRINTVC
"The command PRINTVC is used to output unsimplified verfication
conditions.  'PRINTVC;' prints out all of these on the
terminal.  'PRINTVC X;' prints out all of the VC's for procedure X.
'PRINTVC X 3;' prints the third VC for procedure X.
(PRINTVC (F)) prints out all VC's to file F, which is replaced
if it was previously present.  (PRINTVC (F) X) prints out all
VC's for procedure X on file F. OUTPUT TO FILES IS NOT IMPLEMENTED !!!
The outer block of a program is currently called MAIN. It will
remove VC's for a procedure named MAIN, if one is present!"

READ
"The READ command parses input (programs or rules).
'READ;' accepts input from the teletype.
'READ X;' will try to take input from the file X, where X is
a standard filename (e.g. FOO.BAR[DOT,WIZ]).
The parser calls the verification condition generator, but does
not do simplification.  For this, the command SIMPLIFY must be
used. The syntactic scan and semantic routines should NEVER
bomb out, no matter what string you give them.  If they do,
send a note to RAK and SAVE the program!!!"

READVC
"The command READVC is used to input verification conditions in
external format that were dumped by either a PRINTVC, SIMPLIFY,
or RESIMPLIFY command.  READVC takes a file name in the same
format as READ.   It will expect that file to be a list of
VCs in external format as output by the system.  All previously
existing VCs are deleted and all VCs in the file are loaded.
Note that you may use READVC to continue from a partially
simplified VC dumped by SIMPLIFY.  When used from the terminal,
READVC expects a list of one or more of the form NAME VC,
terminated by a period.  It is probably best to enclose the 
last VC in parenthesis, as the final period is frequently
mistaken for a record -field indicator."


SIMPINIT
"The SIMPINIT command is used to reinitialize the simplifier.  It
should be called whenever a simplification has terminated incorrectly,
for example, in a breakpoint.   In MACLISP, incant <control>G to 
escape from a breakpoint.   In general use, you will never have to do
(SIMPINIT). SIMPINIT is not available at the command toplevel."

SIMPLIFY
"The command SIMPLIFY is used to call the simplifier and output
simplified verification conditions.  The procedure and output
file specifications are the same as for PRINTVC.  Use
'HELP PRINTVC;' to see these conventions."

SHOW
"The command SHOW displays the values of system switches. 'SHOW;'
displays all switches, 'SHOW switch;' displays the value of
switch (if it is a switch). To see the list of available switches,
type 'HELP SWITCHES;'."

STATUS
"The command STATUS prints out a list of the vc's, rulefiles and
rules currently loaded."

SWITCHES
"The verifier is controlled by some switches whose values can be set
by the user.  The following list gives their names and the type of
their values (natnum: an integer greater than or equal to zero; bool:
T or NIL):
RULE		bool	enable rule handler.
DEPTHTALK	bool	signal whenever a depth bound is reached.
PROOFDEPTH	natnum	maximum backwards proof depth.
ASSERTDEPTH	natnum	maximum forwards assertion depth.
CASEDEPTH	natnum	maximum depth of nesting of forwards cases.
SHOWFACT	bool	enable assertion display during proof.
SHOWGOAL	bool	enable subgoal display during proof.
SHOWTEST	bool	enable display of tests made during proof.
SUMMATCH 	bool	enable special sum matching: extra subspace
			instance.
TRACE		bool	enable proof tracing.
TRACEVC		bool	enable display of intermediate VC during proof.
TRACEFACT	bool	enable display of assertions made in trace
				output (works only if TRACE is set).
Current default values can be found out with the SHOW command."

SYSTEM
"The verification system consists of the parser, the verification
condition generator, and the prover parts. The system comes in three
varieties: the full system, the vc-generator, called VCGEN, consisting
of parser and VCG, and the prover, called VPROVE. It is advisable to
keep down core size by using VCGEN, dumping VC's and rules onto files
and loading these into VPROVE.  If a particular function is not
available in a subsystem (like READ in VPROVE) you will get an
appropriate message."

TOPLEVEL
"The toplevel of the verifier consists of a read-eval-loop that parses
and executes various commands. A system command consists of a command
keyword, possibly followed by some arguments, and a terminating ;. The
semicolon must always be present (if it is omitted, the system will
prompt you with '>' to indicate that more input is expected). The
toplevel commands are documented in the file TOPLEV[DOC,VER].
Explanations are also provided by the HELP command (type 'HELP
<command-keyword>;' - 'HELP WHAT;' gives a list of keywords)."

VC
"This command is not intended for general use.
(VC @procname) sets up and calls the verification condition generator.
It requires that the name be a procedue or function, with internal
format dumped by the parser.  This dumping usually requires that
DUMPINTERNAL be set (which see) when parsing the procedure."

END
)